H-Termination proof of /home/matraf/haskell/eval_FullyBlown

YES 4.223 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:

↳ HASKELL

  ↳ BR

mainModule Main

((isHexDigit :: Char -> Bool) :: -> Char Bool)

module Main where

import qualified Prelude

Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

mainModule Main

((isHexDigit :: Char -> Bool) :: -> Char Bool)

module Main where

import qualified Prelude

Cond Reductions:
The following Function with conditions

undefined

| False

= undefined

is transformed to

undefined = undefined1

undefined0 True = undefined

undefined1 = undefined0 False

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

mainModule Main

((isHexDigit :: Char -> Bool) :: -> Char Bool)

module Main where

import qualified Prelude

Num Reduction: All numbers are transformed to thier corresponding representation with Pos, Neg, Succ and Zero.

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

mainModule Main

(isHexDigit :: -> Char Bool)

module Main where

import qualified Prelude

Haskell To QDPs

digraph dp_graph {
node [outthreshold=100, inthreshold=100];1[label="isHexDigit",fontsize=16,color="grey",shape="box"];1 -> 3[label="",style="dashed", color="grey", weight=3];
3[label="isHexDigit vx3",fontsize=16,color="black",shape="triangle"];3 -> 4[label="",style="solid", color="black", weight=3];
4 -> 24[label="",style="dashed", color="red", weight=0];
4[label="isDigit vx3 || vx3 >= Char (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) && vx3 <= Char (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) || vx3 >= Char (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) && vx3 <= Char (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))",fontsize=16,color="magenta"];4 -> 25[label="",style="dashed", color="magenta", weight=3];
4 -> 26[label="",style="dashed", color="magenta", weight=3];
4 -> 27[label="",style="dashed", color="magenta", weight=3];
4 -> 28[label="",style="dashed", color="magenta", weight=3];
4 -> 29[label="",style="dashed", color="magenta", weight=3];
25[label="Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))",fontsize=16,color="green",shape="box"];26[label="Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))",fontsize=16,color="green",shape="box"];27[label="Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))",fontsize=16,color="green",shape="box"];28[label="Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))",fontsize=16,color="green",shape="box"];29[label="vx3",fontsize=16,color="green",shape="box"];24[label="isDigit vx17 || vx17 >= Char (Succ vx18) && vx17 <= Char (Succ vx19) || vx17 >= Char (Succ vx20) && vx17 <= Char (Succ vx21)",fontsize=16,color="black",shape="triangle"];24 -> 35[label="",style="solid", color="black", weight=3];
35 -> 43[label="",style="dashed", color="red", weight=0];
35[label="vx17 >= Char (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))))))))))))))))))))))))))))))))))))))))) && vx17 <= Char (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))))))))))))))))))))))))))))))))))))))))))))))))) || vx17 >= Char (Succ vx18) && vx17 <= Char (Succ vx19) || vx17 >= Char (Succ vx20) && vx17 <= Char (Succ vx21)",fontsize=16,color="magenta"];35 -> 44[label="",style="dashed", color="magenta", weight=3];
35 -> 45[label="",style="dashed", color="magenta", weight=3];
35 -> 46[label="",style="dashed", color="magenta", weight=3];
35 -> 47[label="",style="dashed", color="magenta", weight=3];
35 -> 48[label="",style="dashed", color="magenta", weight=3];
35 -> 49[label="",style="dashed", color="magenta", weight=3];
35 -> 50[label="",style="dashed", color="magenta", weight=3];
44[label="vx17",fontsize=16,color="green",shape="box"];45[label="vx18",fontsize=16,color="green",shape="box"];46[label="Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))",fontsize=16,color="green",shape="box"];47[label="vx19",fontsize=16,color="green",shape="box"];48[label="vx20",fontsize=16,color="green",shape="box"];49[label="vx21",fontsize=16,color="green",shape="box"];50[label="Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))))))))))))))))))))))))))))))))))))))",fontsize=16,color="green",shape="box"];43[label="vx30 >= Char (Succ vx31) && vx30 <= Char (Succ vx32) || vx30 >= Char (Succ vx33) && vx30 <= Char (Succ vx34) || vx30 >= Char (Succ vx35) && vx30 <= Char (Succ vx36)",fontsize=16,color="black",shape="triangle"];43 -> 58[label="",style="solid", color="black", weight=3];
58[label="compare vx30 (Char (Succ vx31)) /= LT && vx30 <= Char (Succ vx32) || vx30 >= Char (Succ vx33) && vx30 <= Char (Succ vx34) || vx30 >= Char (Succ vx35) && vx30 <= Char (Succ vx36)",fontsize=16,color="black",shape="box"];58 -> 59[label="",style="solid", color="black", weight=3];
59[label="not (compare vx30 (Char (Succ vx31)) == LT) && vx30 <= Char (Succ vx32) || vx30 >= Char (Succ vx33) && vx30 <= Char (Succ vx34) || vx30 >= Char (Succ vx35) && vx30 <= Char (Succ vx36)",fontsize=16,color="black",shape="box"];59 -> 60[label="",style="solid", color="black", weight=3];
60[label="not (primCmpChar vx30 (Char (Succ vx31)) == LT) && vx30 <= Char (Succ vx32) || vx30 >= Char (Succ vx33) && vx30 <= Char (Succ vx34) || vx30 >= Char (Succ vx35) && vx30 <= Char (Succ vx36)",fontsize=16,color="burlywood",shape="box"];713[label="vx30/Char vx300",fontsize=10,color="white",style="solid",shape="box"];60 -> 713[label="",style="solid", color="burlywood", weight=9];
713 -> 61[label="",style="solid", color="burlywood", weight=3];
61[label="not (primCmpChar (Char vx300) (Char (Succ vx31)) == LT) && Char vx300 <= Char (Succ vx32) || Char vx300 >= Char (Succ vx33) && Char vx300 <= Char (Succ vx34) || Char vx300 >= Char (Succ vx35) && Char vx300 <= Char (Succ vx36)",fontsize=16,color="black",shape="box"];61 -> 62[label="",style="solid", color="black", weight=3];
62[label="not (primCmpNat vx300 (Succ vx31) == LT) && Char vx300 <= Char (Succ vx32) || Char vx300 >= Char (Succ vx33) && Char vx300 <= Char (Succ vx34) || Char vx300 >= Char (Succ vx35) && Char vx300 <= Char (Succ vx36)",fontsize=16,color="burlywood",shape="box"];714[label="vx300/Succ vx3000",fontsize=10,color="white",style="solid",shape="box"];62 -> 714[label="",style="solid", color="burlywood", weight=9];
714 -> 63[label="",style="solid", color="burlywood", weight=3];
715[label="vx300/Zero",fontsize=10,color="white",style="solid",shape="box"];62 -> 715[label="",style="solid", color="burlywood", weight=9];
715 -> 64[label="",style="solid", color="burlywood", weight=3];
63[label="not (primCmpNat (Succ vx3000) (Succ vx31) == LT) && Char (Succ vx3000) <= Char (Succ vx32) || Char (Succ vx3000) >= Char (Succ vx33) && Char (Succ vx3000) <= Char (Succ vx34) || Char (Succ vx3000) >= Char (Succ vx35) && Char (Succ vx3000) <= Char (Succ vx36)",fontsize=16,color="black",shape="box"];63 -> 65[label="",style="solid", color="black", weight=3];
64[label="not (primCmpNat Zero (Succ vx31) == LT) && Char Zero <= Char (Succ vx32) || Char Zero >= Char (Succ vx33) && Char Zero <= Char (Succ vx34) || Char Zero >= Char (Succ vx35) && Char Zero <= Char (Succ vx36)",fontsize=16,color="black",shape="box"];64 -> 66[label="",style="solid", color="black", weight=3];
65 -> 468[label="",style="dashed", color="red", weight=0];
65[label="not (primCmpNat vx3000 vx31 == LT) && Char (Succ vx3000) <= Char (Succ vx32) || Char (Succ vx3000) >= Char (Succ vx33) && Char (Succ vx3000) <= Char (Succ vx34) || Char (Succ vx3000) >= Char (Succ vx35) && Char (Succ vx3000) <= Char (Succ vx36)",fontsize=16,color="magenta"];65 -> 469[label="",style="dashed", color="magenta", weight=3];
65 -> 470[label="",style="dashed", color="magenta", weight=3];
65 -> 471[label="",style="dashed", color="magenta", weight=3];
65 -> 472[label="",style="dashed", color="magenta", weight=3];
65 -> 473[label="",style="dashed", color="magenta", weight=3];
66[label="not (LT == LT) && Char Zero <= Char (Succ vx32) || Char Zero >= Char (Succ vx33) && Char Zero <= Char (Succ vx34) || Char Zero >= Char (Succ vx35) && Char Zero <= Char (Succ vx36)",fontsize=16,color="black",shape="box"];66 -> 69[label="",style="solid", color="black", weight=3];
469[label="vx3000",fontsize=16,color="green",shape="box"];470[label="Char (Succ vx3000) >= Char (Succ vx33) && Char (Succ vx3000) <= Char (Succ vx34) || Char (Succ vx3000) >= Char (Succ vx35) && Char (Succ vx3000) <= Char (Succ vx36)",fontsize=16,color="black",shape="box"];470 -> 534[label="",style="solid", color="black", weight=3];
471[label="vx3000",fontsize=16,color="green",shape="box"];472[label="vx31",fontsize=16,color="green",shape="box"];473[label="vx32",fontsize=16,color="green",shape="box"];468[label="not (primCmpNat vx53 vx54 == LT) && Char (Succ vx55) <= Char (Succ vx56) || vx57",fontsize=16,color="burlywood",shape="triangle"];717[label="vx53/Succ vx530",fontsize=10,color="white",style="solid",shape="box"];468 -> 717[label="",style="solid", color="burlywood", weight=9];
717 -> 535[label="",style="solid", color="burlywood", weight=3];
718[label="vx53/Zero",fontsize=10,color="white",style="solid",shape="box"];468 -> 718[label="",style="solid", color="burlywood", weight=9];
718 -> 536[label="",style="solid", color="burlywood", weight=3];
69[label="not True && Char Zero <= Char (Succ vx32) || Char Zero >= Char (Succ vx33) && Char Zero <= Char (Succ vx34) || Char Zero >= Char (Succ vx35) && Char Zero <= Char (Succ vx36)",fontsize=16,color="black",shape="box"];69 -> 74[label="",style="solid", color="black", weight=3];
534[label="compare (Char (Succ vx3000)) (Char (Succ vx33)) /= LT && Char (Succ vx3000) <= Char (Succ vx34) || Char (Succ vx3000) >= Char (Succ vx35) && Char (Succ vx3000) <= Char (Succ vx36)",fontsize=16,color="black",shape="box"];534 -> 537[label="",style="solid", color="black", weight=3];
535[label="not (primCmpNat (Succ vx530) vx54 == LT) && Char (Succ vx55) <= Char (Succ vx56) || vx57",fontsize=16,color="burlywood",shape="box"];719[label="vx54/Succ vx540",fontsize=10,color="white",style="solid",shape="box"];535 -> 719[label="",style="solid", color="burlywood", weight=9];
719 -> 538[label="",style="solid", color="burlywood", weight=3];
720[label="vx54/Zero",fontsize=10,color="white",style="solid",shape="box"];535 -> 720[label="",style="solid", color="burlywood", weight=9];
720 -> 539[label="",style="solid", color="burlywood", weight=3];
536[label="not (primCmpNat Zero vx54 == LT) && Char (Succ vx55) <= Char (Succ vx56) || vx57",fontsize=16,color="burlywood",shape="box"];721[label="vx54/Succ vx540",fontsize=10,color="white",style="solid",shape="box"];536 -> 721[label="",style="solid", color="burlywood", weight=9];
721 -> 540[label="",style="solid", color="burlywood", weight=3];
722[label="vx54/Zero",fontsize=10,color="white",style="solid",shape="box"];536 -> 722[label="",style="solid", color="burlywood", weight=9];
722 -> 541[label="",style="solid", color="burlywood", weight=3];
74[label="False && Char Zero <= Char (Succ vx32) || Char Zero >= Char (Succ vx33) && Char Zero <= Char (Succ vx34) || Char Zero >= Char (Succ vx35) && Char Zero <= Char (Succ vx36)",fontsize=16,color="black",shape="box"];74 -> 79[label="",style="solid", color="black", weight=3];
537[label="not (compare (Char (Succ vx3000)) (Char (Succ vx33)) == LT) && Char (Succ vx3000) <= Char (Succ vx34) || Char (Succ vx3000) >= Char (Succ vx35) && Char (Succ vx3000) <= Char (Succ vx36)",fontsize=16,color="black",shape="box"];537 -> 542[label="",style="solid", color="black", weight=3];
538[label="not (primCmpNat (Succ vx530) (Succ vx540) == LT) && Char (Succ vx55) <= Char (Succ vx56) || vx57",fontsize=16,color="black",shape="box"];538 -> 543[label="",style="solid", color="black", weight=3];
539[label="not (primCmpNat (Succ vx530) Zero == LT) && Char (Succ vx55) <= Char (Succ vx56) || vx57",fontsize=16,color="black",shape="box"];539 -> 544[label="",style="solid", color="black", weight=3];
540[label="not (primCmpNat Zero (Succ vx540) == LT) && Char (Succ vx55) <= Char (Succ vx56) || vx57",fontsize=16,color="black",shape="box"];540 -> 545[label="",style="solid", color="black", weight=3];
541[label="not (primCmpNat Zero Zero == LT) && Char (Succ vx55) <= Char (Succ vx56) || vx57",fontsize=16,color="black",shape="box"];541 -> 546[label="",style="solid", color="black", weight=3];
79[label="False || Char Zero >= Char (Succ vx33) && Char Zero <= Char (Succ vx34) || Char Zero >= Char (Succ vx35) && Char Zero <= Char (Succ vx36)",fontsize=16,color="black",shape="box"];79 -> 85[label="",style="solid", color="black", weight=3];
542[label="not (primCmpChar (Char (Succ vx3000)) (Char (Succ vx33)) == LT) && Char (Succ vx3000) <= Char (Succ vx34) || Char (Succ vx3000) >= Char (Succ vx35) && Char (Succ vx3000) <= Char (Succ vx36)",fontsize=16,color="black",shape="box"];542 -> 547[label="",style="solid", color="black", weight=3];
543 -> 468[label="",style="dashed", color="red", weight=0];
543[label="not (primCmpNat vx530 vx540 == LT) && Char (Succ vx55) <= Char (Succ vx56) || vx57",fontsize=16,color="magenta"];543 -> 548[label="",style="dashed", color="magenta", weight=3];
543 -> 549[label="",style="dashed", color="magenta", weight=3];
544[label="not (GT == LT) && Char (Succ vx55) <= Char (Succ vx56) || vx57",fontsize=16,color="black",shape="box"];544 -> 550[label="",style="solid", color="black", weight=3];
545[label="not (LT == LT) && Char (Succ vx55) <= Char (Succ vx56) || vx57",fontsize=16,color="black",shape="box"];545 -> 551[label="",style="solid", color="black", weight=3];
546[label="not (EQ == LT) && Char (Succ vx55) <= Char (Succ vx56) || vx57",fontsize=16,color="black",shape="box"];546 -> 552[label="",style="solid", color="black", weight=3];
85[label="Char Zero >= Char (Succ vx33) && Char Zero <= Char (Succ vx34) || Char Zero >= Char (Succ vx35) && Char Zero <= Char (Succ vx36)",fontsize=16,color="black",shape="box"];85 -> 93[label="",style="solid", color="black", weight=3];
547 -> 468[label="",style="dashed", color="red", weight=0];
547[label="not (primCmpNat (Succ vx3000) (Succ vx33) == LT) && Char (Succ vx3000) <= Char (Succ vx34) || Char (Succ vx3000) >= Char (Succ vx35) && Char (Succ vx3000) <= Char (Succ vx36)",fontsize=16,color="magenta"];547 -> 553[label="",style="dashed", color="magenta", weight=3];
547 -> 554[label="",style="dashed", color="magenta", weight=3];
547 -> 555[label="",style="dashed", color="magenta", weight=3];
547 -> 556[label="",style="dashed", color="magenta", weight=3];
547 -> 557[label="",style="dashed", color="magenta", weight=3];
548[label="vx530",fontsize=16,color="green",shape="box"];549[label="vx540",fontsize=16,color="green",shape="box"];550[label="not False && Char (Succ vx55) <= Char (Succ vx56) || vx57",fontsize=16,color="black",shape="triangle"];550 -> 558[label="",style="solid", color="black", weight=3];
551[label="not True && Char (Succ vx55) <= Char (Succ vx56) || vx57",fontsize=16,color="black",shape="box"];551 -> 559[label="",style="solid", color="black", weight=3];
552 -> 550[label="",style="dashed", color="red", weight=0];
552[label="not False && Char (Succ vx55) <= Char (Succ vx56) || vx57",fontsize=16,color="magenta"];93[label="compare (Char Zero) (Char (Succ vx33)) /= LT && Char Zero <= Char (Succ vx34) || Char Zero >= Char (Succ vx35) && Char Zero <= Char (Succ vx36)",fontsize=16,color="black",shape="box"];93 -> 101[label="",style="solid", color="black", weight=3];
553[label="vx3000",fontsize=16,color="green",shape="box"];554[label="Char (Succ vx3000) >= Char (Succ vx35) && Char (Succ vx3000) <= Char (Succ vx36)",fontsize=16,color="black",shape="box"];554 -> 560[label="",style="solid", color="black", weight=3];
555[label="Succ vx3000",fontsize=16,color="green",shape="box"];556[label="Succ vx33",fontsize=16,color="green",shape="box"];557[label="vx34",fontsize=16,color="green",shape="box"];558[label="True && Char (Succ vx55) <= Char (Succ vx56) || vx57",fontsize=16,color="black",shape="box"];558 -> 561[label="",style="solid", color="black", weight=3];
559[label="False && Char (Succ vx55) <= Char (Succ vx56) || vx57",fontsize=16,color="black",shape="box"];559 -> 562[label="",style="solid", color="black", weight=3];
101[label="not (compare (Char Zero) (Char (Succ vx33)) == LT) && Char Zero <= Char (Succ vx34) || Char Zero >= Char (Succ vx35) && Char Zero <= Char (Succ vx36)",fontsize=16,color="black",shape="box"];101 -> 110[label="",style="solid", color="black", weight=3];
560[label="compare (Char (Succ vx3000)) (Char (Succ vx35)) /= LT && Char (Succ vx3000) <= Char (Succ vx36)",fontsize=16,color="black",shape="box"];560 -> 563[label="",style="solid", color="black", weight=3];
561[label="Char (Succ vx55) <= Char (Succ vx56) || vx57",fontsize=16,color="black",shape="box"];561 -> 564[label="",style="solid", color="black", weight=3];
562[label="False || vx57",fontsize=16,color="black",shape="triangle"];562 -> 565[label="",style="solid", color="black", weight=3];
110[label="not (primCmpChar (Char Zero) (Char (Succ vx33)) == LT) && Char Zero <= Char (Succ vx34) || Char Zero >= Char (Succ vx35) && Char Zero <= Char (Succ vx36)",fontsize=16,color="black",shape="box"];110 -> 121[label="",style="solid", color="black", weight=3];
563[label="not (compare (Char (Succ vx3000)) (Char (Succ vx35)) == LT) && Char (Succ vx3000) <= Char (Succ vx36)",fontsize=16,color="black",shape="box"];563 -> 566[label="",style="solid", color="black", weight=3];
564[label="compare (Char (Succ vx55)) (Char (Succ vx56)) /= GT || vx57",fontsize=16,color="black",shape="box"];564 -> 567[label="",style="solid", color="black", weight=3];
565[label="vx57",fontsize=16,color="green",shape="box"];121[label="not (primCmpNat Zero (Succ vx33) == LT) && Char Zero <= Char (Succ vx34) || Char Zero >= Char (Succ vx35) && Char Zero <= Char (Succ vx36)",fontsize=16,color="black",shape="box"];121 -> 130[label="",style="solid", color="black", weight=3];
566[label="not (primCmpChar (Char (Succ vx3000)) (Char (Succ vx35)) == LT) && Char (Succ vx3000) <= Char (Succ vx36)",fontsize=16,color="black",shape="box"];566 -> 568[label="",style="solid", color="black", weight=3];
567[label="not (compare (Char (Succ vx55)) (Char (Succ vx56)) == GT) || vx57",fontsize=16,color="black",shape="box"];567 -> 569[label="",style="solid", color="black", weight=3];
130[label="not (LT == LT) && Char Zero <= Char (Succ vx34) || Char Zero >= Char (Succ vx35) && Char Zero <= Char (Succ vx36)",fontsize=16,color="black",shape="box"];130 -> 140[label="",style="solid", color="black", weight=3];
568 -> 648[label="",style="dashed", color="red", weight=0];
568[label="not (primCmpNat (Succ vx3000) (Succ vx35) == LT) && Char (Succ vx3000) <= Char (Succ vx36)",fontsize=16,color="magenta"];568 -> 649[label="",style="dashed", color="magenta", weight=3];
568 -> 650[label="",style="dashed", color="magenta", weight=3];
568 -> 651[label="",style="dashed", color="magenta", weight=3];
569[label="not (primCmpChar (Char (Succ vx55)) (Char (Succ vx56)) == GT) || vx57",fontsize=16,color="black",shape="box"];569 -> 571[label="",style="solid", color="black", weight=3];
140[label="not True && Char Zero <= Char (Succ vx34) || Char Zero >= Char (Succ vx35) && Char Zero <= Char (Succ vx36)",fontsize=16,color="black",shape="box"];140 -> 151[label="",style="solid", color="black", weight=3];
649[label="Succ vx35",fontsize=16,color="green",shape="box"];650[label="Succ vx3000",fontsize=16,color="green",shape="box"];651[label="Char (Succ vx3000) <= Char (Succ vx36)",fontsize=16,color="black",shape="box"];651 -> 665[label="",style="solid", color="black", weight=3];
648[label="not (primCmpNat vx3000000 vx35000 == LT) && vx59",fontsize=16,color="burlywood",shape="triangle"];727[label="vx3000000/Succ vx30000000",fontsize=10,color="white",style="solid",shape="box"];648 -> 727[label="",style="solid", color="burlywood", weight=9];
727 -> 666[label="",style="solid", color="burlywood", weight=3];
728[label="vx3000000/Zero",fontsize=10,color="white",style="solid",shape="box"];648 -> 728[label="",style="solid", color="burlywood", weight=9];
728 -> 667[label="",style="solid", color="burlywood", weight=3];
571[label="not (primCmpNat (Succ vx55) (Succ vx56) == GT) || vx57",fontsize=16,color="black",shape="box"];571 -> 574[label="",style="solid", color="black", weight=3];
151[label="False && Char Zero <= Char (Succ vx34) || Char Zero >= Char (Succ vx35) && Char Zero <= Char (Succ vx36)",fontsize=16,color="black",shape="box"];151 -> 162[label="",style="solid", color="black", weight=3];
665[label="compare (Char (Succ vx3000)) (Char (Succ vx36)) /= GT",fontsize=16,color="black",shape="box"];665 -> 669[label="",style="solid", color="black", weight=3];
666[label="not (primCmpNat (Succ vx30000000) vx35000 == LT) && vx59",fontsize=16,color="burlywood",shape="box"];729[label="vx35000/Succ vx350000",fontsize=10,color="white",style="solid",shape="box"];666 -> 729[label="",style="solid", color="burlywood", weight=9];
729 -> 670[label="",style="solid", color="burlywood", weight=3];
730[label="vx35000/Zero",fontsize=10,color="white",style="solid",shape="box"];666 -> 730[label="",style="solid", color="burlywood", weight=9];
730 -> 671[label="",style="solid", color="burlywood", weight=3];
667[label="not (primCmpNat Zero vx35000 == LT) && vx59",fontsize=16,color="burlywood",shape="box"];731[label="vx35000/Succ vx350000",fontsize=10,color="white",style="solid",shape="box"];667 -> 731[label="",style="solid", color="burlywood", weight=9];
731 -> 672[label="",style="solid", color="burlywood", weight=3];
732[label="vx35000/Zero",fontsize=10,color="white",style="solid",shape="box"];667 -> 732[label="",style="solid", color="burlywood", weight=9];
732 -> 673[label="",style="solid", color="burlywood", weight=3];
574[label="not (primCmpNat vx55 vx56 == GT) || vx57",fontsize=16,color="burlywood",shape="triangle"];733[label="vx55/Succ vx550",fontsize=10,color="white",style="solid",shape="box"];574 -> 733[label="",style="solid", color="burlywood", weight=9];
733 -> 579[label="",style="solid", color="burlywood", weight=3];
734[label="vx55/Zero",fontsize=10,color="white",style="solid",shape="box"];574 -> 734[label="",style="solid", color="burlywood", weight=9];
734 -> 580[label="",style="solid", color="burlywood", weight=3];
162[label="False || Char Zero >= Char (Succ vx35) && Char Zero <= Char (Succ vx36)",fontsize=16,color="black",shape="box"];162 -> 176[label="",style="solid", color="black", weight=3];
669[label="not (compare (Char (Succ vx3000)) (Char (Succ vx36)) == GT)",fontsize=16,color="black",shape="box"];669 -> 675[label="",style="solid", color="black", weight=3];
670[label="not (primCmpNat (Succ vx30000000) (Succ vx350000) == LT) && vx59",fontsize=16,color="black",shape="box"];670 -> 676[label="",style="solid", color="black", weight=3];
671[label="not (primCmpNat (Succ vx30000000) Zero == LT) && vx59",fontsize=16,color="black",shape="box"];671 -> 677[label="",style="solid", color="black", weight=3];
672[label="not (primCmpNat Zero (Succ vx350000) == LT) && vx59",fontsize=16,color="black",shape="box"];672 -> 678[label="",style="solid", color="black", weight=3];
673[label="not (primCmpNat Zero Zero == LT) && vx59",fontsize=16,color="black",shape="box"];673 -> 679[label="",style="solid", color="black", weight=3];
579[label="not (primCmpNat (Succ vx550) vx56 == GT) || vx57",fontsize=16,color="burlywood",shape="box"];735[label="vx56/Succ vx560",fontsize=10,color="white",style="solid",shape="box"];579 -> 735[label="",style="solid", color="burlywood", weight=9];
735 -> 585[label="",style="solid", color="burlywood", weight=3];
736[label="vx56/Zero",fontsize=10,color="white",style="solid",shape="box"];579 -> 736[label="",style="solid", color="burlywood", weight=9];
736 -> 586[label="",style="solid", color="burlywood", weight=3];
580[label="not (primCmpNat Zero vx56 == GT) || vx57",fontsize=16,color="burlywood",shape="box"];737[label="vx56/Succ vx560",fontsize=10,color="white",style="solid",shape="box"];580 -> 737[label="",style="solid", color="burlywood", weight=9];
737 -> 587[label="",style="solid", color="burlywood", weight=3];
738[label="vx56/Zero",fontsize=10,color="white",style="solid",shape="box"];580 -> 738[label="",style="solid", color="burlywood", weight=9];
738 -> 588[label="",style="solid", color="burlywood", weight=3];
176[label="Char Zero >= Char (Succ vx35) && Char Zero <= Char (Succ vx36)",fontsize=16,color="black",shape="box"];176 -> 192[label="",style="solid", color="black", weight=3];
675[label="not (primCmpChar (Char (Succ vx3000)) (Char (Succ vx36)) == GT)",fontsize=16,color="black",shape="box"];675 -> 681[label="",style="solid", color="black", weight=3];
676 -> 648[label="",style="dashed", color="red", weight=0];
676[label="not (primCmpNat vx30000000 vx350000 == LT) && vx59",fontsize=16,color="magenta"];676 -> 682[label="",style="dashed", color="magenta", weight=3];
676 -> 683[label="",style="dashed", color="magenta", weight=3];
677[label="not (GT == LT) && vx59",fontsize=16,color="black",shape="box"];677 -> 684[label="",style="solid", color="black", weight=3];
678[label="not (LT == LT) && vx59",fontsize=16,color="black",shape="box"];678 -> 685[label="",style="solid", color="black", weight=3];
679[label="not (EQ == LT) && vx59",fontsize=16,color="black",shape="box"];679 -> 686[label="",style="solid", color="black", weight=3];
585[label="not (primCmpNat (Succ vx550) (Succ vx560) == GT) || vx57",fontsize=16,color="black",shape="box"];585 -> 594[label="",style="solid", color="black", weight=3];
586[label="not (primCmpNat (Succ vx550) Zero == GT) || vx57",fontsize=16,color="black",shape="box"];586 -> 595[label="",style="solid", color="black", weight=3];
587[label="not (primCmpNat Zero (Succ vx560) == GT) || vx57",fontsize=16,color="black",shape="box"];587 -> 596[label="",style="solid", color="black", weight=3];
588[label="not (primCmpNat Zero Zero == GT) || vx57",fontsize=16,color="black",shape="box"];588 -> 597[label="",style="solid", color="black", weight=3];
192[label="compare (Char Zero) (Char (Succ vx35)) /= LT && Char Zero <= Char (Succ vx36)",fontsize=16,color="black",shape="box"];192 -> 209[label="",style="solid", color="black", weight=3];
681[label="not (primCmpNat (Succ vx3000) (Succ vx36) == GT)",fontsize=16,color="black",shape="box"];681 -> 688[label="",style="solid", color="black", weight=3];
682[label="vx350000",fontsize=16,color="green",shape="box"];683[label="vx30000000",fontsize=16,color="green",shape="box"];684[label="not False && vx59",fontsize=16,color="black",shape="triangle"];684 -> 689[label="",style="solid", color="black", weight=3];
685[label="not True && vx59",fontsize=16,color="black",shape="box"];685 -> 690[label="",style="solid", color="black", weight=3];
686 -> 684[label="",style="dashed", color="red", weight=0];
686[label="not False && vx59",fontsize=16,color="magenta"];594 -> 574[label="",style="dashed", color="red", weight=0];
594[label="not (primCmpNat vx550 vx560 == GT) || vx57",fontsize=16,color="magenta"];594 -> 605[label="",style="dashed", color="magenta", weight=3];
594 -> 606[label="",style="dashed", color="magenta", weight=3];
595[label="not (GT == GT) || vx57",fontsize=16,color="black",shape="box"];595 -> 607[label="",style="solid", color="black", weight=3];
596[label="not (LT == GT) || vx57",fontsize=16,color="black",shape="box"];596 -> 608[label="",style="solid", color="black", weight=3];
597[label="not (EQ == GT) || vx57",fontsize=16,color="black",shape="box"];597 -> 609[label="",style="solid", color="black", weight=3];
209[label="not (compare (Char Zero) (Char (Succ vx35)) == LT) && Char Zero <= Char (Succ vx36)",fontsize=16,color="black",shape="box"];209 -> 252[label="",style="solid", color="black", weight=3];
688[label="not (primCmpNat vx3000 vx36 == GT)",fontsize=16,color="burlywood",shape="triangle"];742[label="vx3000/Succ vx30000",fontsize=10,color="white",style="solid",shape="box"];688 -> 742[label="",style="solid", color="burlywood", weight=9];
742 -> 692[label="",style="solid", color="burlywood", weight=3];
743[label="vx3000/Zero",fontsize=10,color="white",style="solid",shape="box"];688 -> 743[label="",style="solid", color="burlywood", weight=9];
743 -> 693[label="",style="solid", color="burlywood", weight=3];
689[label="True && vx59",fontsize=16,color="black",shape="box"];689 -> 694[label="",style="solid", color="black", weight=3];
690[label="False && vx59",fontsize=16,color="black",shape="box"];690 -> 695[label="",style="solid", color="black", weight=3];
605[label="vx550",fontsize=16,color="green",shape="box"];606[label="vx560",fontsize=16,color="green",shape="box"];607[label="not True || vx57",fontsize=16,color="black",shape="box"];607 -> 617[label="",style="solid", color="black", weight=3];
608[label="not False || vx57",fontsize=16,color="black",shape="triangle"];608 -> 618[label="",style="solid", color="black", weight=3];
609 -> 608[label="",style="dashed", color="red", weight=0];
609[label="not False || vx57",fontsize=16,color="magenta"];252[label="not (primCmpChar (Char Zero) (Char (Succ vx35)) == LT) && Char Zero <= Char (Succ vx36)",fontsize=16,color="black",shape="box"];252 -> 268[label="",style="solid", color="black", weight=3];
692[label="not (primCmpNat (Succ vx30000) vx36 == GT)",fontsize=16,color="burlywood",shape="box"];745[label="vx36/Succ vx360",fontsize=10,color="white",style="solid",shape="box"];692 -> 745[label="",style="solid", color="burlywood", weight=9];
745 -> 697[label="",style="solid", color="burlywood", weight=3];
746[label="vx36/Zero",fontsize=10,color="white",style="solid",shape="box"];692 -> 746[label="",style="solid", color="burlywood", weight=9];
746 -> 698[label="",style="solid", color="burlywood", weight=3];
693[label="not (primCmpNat Zero vx36 == GT)",fontsize=16,color="burlywood",shape="box"];747[label="vx36/Succ vx360",fontsize=10,color="white",style="solid",shape="box"];693 -> 747[label="",style="solid", color="burlywood", weight=9];
747 -> 699[label="",style="solid", color="burlywood", weight=3];
748[label="vx36/Zero",fontsize=10,color="white",style="solid",shape="box"];693 -> 748[label="",style="solid", color="burlywood", weight=9];
748 -> 700[label="",style="solid", color="burlywood", weight=3];
694[label="vx59",fontsize=16,color="green",shape="box"];695[label="False",fontsize=16,color="green",shape="box"];617 -> 562[label="",style="dashed", color="red", weight=0];
617[label="False || vx57",fontsize=16,color="magenta"];618[label="True || vx57",fontsize=16,color="black",shape="box"];618 -> 626[label="",style="solid", color="black", weight=3];
268 -> 648[label="",style="dashed", color="red", weight=0];
268[label="not (primCmpNat Zero (Succ vx35) == LT) && Char Zero <= Char (Succ vx36)",fontsize=16,color="magenta"];268 -> 661[label="",style="dashed", color="magenta", weight=3];
268 -> 662[label="",style="dashed", color="magenta", weight=3];
268 -> 663[label="",style="dashed", color="magenta", weight=3];
697[label="not (primCmpNat (Succ vx30000) (Succ vx360) == GT)",fontsize=16,color="black",shape="box"];697 -> 702[label="",style="solid", color="black", weight=3];
698[label="not (primCmpNat (Succ vx30000) Zero == GT)",fontsize=16,color="black",shape="box"];698 -> 703[label="",style="solid", color="black", weight=3];
699[label="not (primCmpNat Zero (Succ vx360) == GT)",fontsize=16,color="black",shape="box"];699 -> 704[label="",style="solid", color="black", weight=3];
700[label="not (primCmpNat Zero Zero == GT)",fontsize=16,color="black",shape="box"];700 -> 705[label="",style="solid", color="black", weight=3];
626[label="True",fontsize=16,color="green",shape="box"];661[label="Succ vx35",fontsize=16,color="green",shape="box"];662[label="Zero",fontsize=16,color="green",shape="box"];663[label="Char Zero <= Char (Succ vx36)",fontsize=16,color="black",shape="box"];663 -> 668[label="",style="solid", color="black", weight=3];
702 -> 688[label="",style="dashed", color="red", weight=0];
702[label="not (primCmpNat vx30000 vx360 == GT)",fontsize=16,color="magenta"];702 -> 706[label="",style="dashed", color="magenta", weight=3];
702 -> 707[label="",style="dashed", color="magenta", weight=3];
703[label="not (GT == GT)",fontsize=16,color="black",shape="box"];703 -> 708[label="",style="solid", color="black", weight=3];
704 -> 691[label="",style="dashed", color="red", weight=0];
704[label="not (LT == GT)",fontsize=16,color="magenta"];705[label="not (EQ == GT)",fontsize=16,color="black",shape="box"];705 -> 709[label="",style="solid", color="black", weight=3];
668[label="compare (Char Zero) (Char (Succ vx36)) /= GT",fontsize=16,color="black",shape="box"];668 -> 674[label="",style="solid", color="black", weight=3];
706[label="vx30000",fontsize=16,color="green",shape="box"];707[label="vx360",fontsize=16,color="green",shape="box"];708[label="not True",fontsize=16,color="black",shape="box"];708 -> 710[label="",style="solid", color="black", weight=3];
691[label="not (LT == GT)",fontsize=16,color="black",shape="triangle"];691 -> 696[label="",style="solid", color="black", weight=3];
709 -> 696[label="",style="dashed", color="red", weight=0];
709[label="not False",fontsize=16,color="magenta"];674[label="not (compare (Char Zero) (Char (Succ vx36)) == GT)",fontsize=16,color="black",shape="box"];674 -> 680[label="",style="solid", color="black", weight=3];
710[label="False",fontsize=16,color="green",shape="box"];696[label="not False",fontsize=16,color="black",shape="triangle"];696 -> 701[label="",style="solid", color="black", weight=3];
680[label="not (primCmpChar (Char Zero) (Char (Succ vx36)) == GT)",fontsize=16,color="black",shape="box"];680 -> 687[label="",style="solid", color="black", weight=3];
701[label="True",fontsize=16,color="green",shape="box"];687[label="not (primCmpNat Zero (Succ vx36) == GT)",fontsize=16,color="black",shape="box"];687 -> 691[label="",style="solid", color="black", weight=3];
}

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                    ↳ QDPSizeChangeProof

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_not(Succ(vx30000), Succ(vx360)) → new_not(vx30000, vx360)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

new_not(Succ(vx30000), Succ(vx360)) → new_not(vx30000, vx360)
The graph contains the following edges 1 > 1, 2 > 2

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPSizeChangeProof

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_asAs(Succ(vx30000000), Succ(vx350000), vx59) → new_asAs(vx30000000, vx350000, vx59)

From the DPs we obtained the following set of size-change graphs:

new_asAs(Succ(vx30000000), Succ(vx350000), vx59) → new_asAs(vx30000000, vx350000, vx59)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPSizeChangeProof

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_pePe(Succ(vx550), Succ(vx560), vx57) → new_pePe(vx550, vx560, vx57)

From the DPs we obtained the following set of size-change graphs:

new_pePe(Succ(vx550), Succ(vx560), vx57) → new_pePe(vx550, vx560, vx57)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_pePe0(Succ(vx530), Succ(vx540), vx55, vx56, vx57) → new_pePe0(vx530, vx540, vx55, vx56, vx57)

From the DPs we obtained the following set of size-change graphs:

new_pePe0(Succ(vx530), Succ(vx540), vx55, vx56, vx57) → new_pePe0(vx530, vx540, vx55, vx56, vx57)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3, 4 >= 4, 5 >= 5